@i stable state.P(state)   == e@i. P((state when e))  P(state after e) 

latex

---

clarification:

es-stable(es;i;state.P(state))
== alle-at(es;i;e.P(es-state-when(es;e))  P(es-state-after(es;e))) 

latex

Definitions	e@i. P(e), P  Q, (state when e), state after e
FDL editor aliases	es-stable